$\forall$${\it es}$:ES, $T$:Type, $i$:Id, $P$:($T$$\rightarrow$Prop), $L$:$T$ List, $Q$:(E$\rightarrow$\{$x$:$T$$\mid$ ($x$ $\in$ $L$) \}$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$T$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ ($\forall$$x$$\in$$L$. $\forall$$e$:E. $Q$($e$,$x$) $\Rightarrow$ loc($e$) $=$ $i$ $\in$ Id)
\\[0ex]$\Rightarrow$ ($\forall$$x$$\in$$L$. $P$($x$) $\Rightarrow$ ($\exists$$e$:E. $Q$($e$,$x$)))
\\[0ex]$\Rightarrow$ ($\neg$($\exists$$x$$\in$$L$.$P$($x$)) $\Rightarrow$ $\exists$${\it e'}$@$i$.True)
\\[0ex]$\Rightarrow$ $\exists$${\it e'}$@$i$.$\forall$$x$$\in$$L$. $P$($x$) $\Rightarrow$ ($\exists$$e$:E. $e$ $\leq$ ${\it e'}$  \& $Q$($e$,$x$))